the_w:World, e, e':E. FairFifo  (e <loc e'  (loc(e) = loc(e')  Id & e <c e')) 

latex

Definitions	P  Q, P  Q, <a, b>, e <loc e', P & Q, x:A  B(x), , s = t, Id, loc(e), e <c e', P  Q, FairFifo, E, x:A. B(x), t  T, World, #$n, R^+, , , {x:A| B(x)} , a < b, f(a), rel_exp(T;R;n), x:AB(x), x.A(x), (i = j), x f y, x:A. B(x), left + right, P  Q, A c B, Type, b, isrcv(k), kind(e), sender(e), time(e)
Lemmas	w-causl-time, w-sender wf, w-ekind wf, isrcv wf, assert wf, nat plus inc, rel exp wf, world wf, w-E wf, fair-fifo wf, w-causl wf, w-loc wf, Id wf, w-locl wf